Inference at * 
Iof proof for Lemma branch wf2:


  P:, d:Dec(P), T:Type, A:(PT), B:(q:P.T). if p:P then A(p) else B fi   T 

latex

 by ((Unfold `branch` ( 0)) 
CollapseTHEN (Auto)) 

latex

Co1: .....subterm..... T:t1:n

Co1: 1. P : 
Co1: 2. d : Dec(P)
Co1: 3. T : Type
Co1: 4. PT
Co1: 5. q:P.T
Co1:   d  (P + (P))
Co2: .....subterm..... T:t3:n

Co2: 1. P : 
Co2: 2. d : Dec(P)
Co2: 3. T : Type
Co2: 4. PT
Co2: 5. B : q:P.T
Co2: 6. x : P
Co2: 7. d = (inr x )
Co2:   B  T
Co.

Definitions

if p:P then A(p) else B fi , Type, case b of inl(x) => s(x) | inr(y) => t(y), False, P  Q, Void, left + right, Dec(P), , x:A. B(x), x:AB(x), t  T, x:A.B(x), A